COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input basic
C00005 ENDMK
C⊗;
\input basic
\def\if{\hbox{\bf\ if }}
\def\then{\hbox{\bf\ then }}
\def\else{\hbox{\bf\ else }}
\def\elseif{\hbox{\bf\ else if }}

\noindent 1. Let the array $A$ be such that initially

$$∀i.(0 ≤ i ≤ n ⊃ A[i] = 1).\eqno(1)$$

	a. (only 5 points) Write a flow chart type program (i.e. with
assignments and {\bf go to}s), not using multiplication or any array other
than $A$, that terminates with

$$∀i.(0 ≤ i ≤ n ⊃ A[i] = {n\choose i},\eqno(2)$$

\noindent i.e. it computes a vector of binomial coefficients.  Remember the recurrence
relation of Pascal's triangle which may be written

%$$\eqalign {{n\choose k} = ⊗\if k < 0 ∨ k > n \then 0\cr
%			⊗\elseif k = 0 ∨ k = n \then 1\cr
%			⊗\else {n-1 \choose k-1} + {n-1\choose k},\cr}\eqno(3)$$
%
$${n\choose k} = \if k < 0 ∨ k > n \then 0
\elseif k = 0 ∨ k = n \then 1
\else {n-1 \choose k-1} + {n-1\choose k},\eqno(3)$$

\noindent but it shouldn't be used directly as a recursive program,
because it recomputes the $j\choose k$ so often that it takes
exponential time.

	b. (20 whole points) Attach sentences of first order logic
to each label in your program so that partial correctness as expressed
by attaching equation (2) to the exit label can be proved by the method
of invariant assertions.

	We just want the assertions -- not the proof.

\par\vfill\eject\end